Double click to show/hide
0: main
14: ERC1155Action.safeBatchTransferFrom
21: FreeCollateralExternal.checkFreeCollateralAndRevert
22: FreeCollateralExternal.checkFreeCollateralAndRevert
23: SettleAssetsExternal.settleAssetsAndReturnPortfolio
24: SettleAssetsExternal.settleAssetsAndReturnPortfolio
25: SettleAssetsExternal.settleAssetsAndFinalize
26: SettleAssetsExternal.settleAssetsAndFinalize
accountContextMustBeReadAndWrittenExactlyOnce-safeBatchTransferFrom(address,address,uint256[],uint256[],bytes)_main 0_0_0_0_0_0_0_0 0_0_0_0_0_0_0_0 14: ERC1155Action.safeBatchTransferFrom 14: ERC1155Action.safeBatchTransferFrom 0_0_0_0_0_0_0_0->14: ERC1155Action.safeBatchTransferFrom 62_0_0_0_0_0_0_0 62_0_0_0_0_0_0_0 14: ERC1155Action.safeBatchTransferFrom->62_0_0_0_0_0_0_0
Block 0_0_0_0_0_0_0_0: W1 = havoc
W2 = havoc
W3 = havoc
R4 = havoc
W5 = havoc
W6 = havoc
W7 = havoc
W8 = havoc
W9 = havoc
W10 = havoc
W11 = havoc
W12 = havoc
W13 = havoc
W14 = havoc
R15 = havoc
R16 = havoc
W36 = havoc
W37 = havoc
UR38 = havoc
UR39 = havoc
args = havoc
R40 = havoc
R41 = havoc
R42 = havoc
R43 = havoc
R44 = havoc
R45 = havoc
e.msg.sender = havoc
e.msg.value = havoc
R46 = havoc
e.msg.address = havoc
R47 = havoc
e.block.number = havoc
e.block.timestamp = havoc
R48 = havoc
M49 = havoc
R50 = havoc
tacCalldatabuf!0@23 = havoc
R51 = havoc
M52 = havoc
R53 = havoc
R54 = havoc
R55 = havoc
R56 = havoc
tacCalldatabuf!0@25 = havoc
R57 = havoc
M58 = havoc
R59 = havoc
R60 = havoc
R61 = havoc
R62 = havoc
tacCalldatabuf!0@24 = havoc
R63 = havoc
M64 = havoc
R65 = havoc
R66 = havoc
R67 = havoc
R68 = havoc
tacCalldatabuf!0@26 = havoc
R69 = havoc
M70 = havoc
R71 = havoc
R72 = havoc
R73 = havoc
R74 = havoc
tacCalldatabuf!0@21 = havoc
R75 = havoc
M76 = havoc
R77 = havoc
tacCalldatabuf!0@22 = havoc
R78 = havoc
M79 = havoc
TRANSIENT::MetaKey(name=cvl.label.start, typ=class java.lang.String)=multi contract setup::
currentContract = 0xce4604a000000000000000000000002a
TRANSIENT::MetaKey(name=cvl.label.end, typ=class java.lang.Boolean)=true::
TRANSIENT::MetaKey(name=cvl.label.start, typ=class java.lang.String)=rule parameters setup::
account = havoc
B80 = (0x0<=account)&&(account<=0xffffffffffffffffffffffffffffffffffffffff)
assume B80
TRANSIENT::MetaKey(name=cvl.label.end, typ=class java.lang.Boolean)=true::
TRANSIENT::MetaKey(name=cvl.label.start, typ=class java.lang.String)=last storage initialize::
B82 = (0x0<=R4)&&(R4<=0xffffffffffffffffffffffffffffffffffffffff)
assume B82
B84 = (0x0<=R15)&&(R15<=0xffffffffffffffffffffffffffffffffffffffff)
assume B84
B86 = (0x0<=R16)&&(R16<=0xffffffffffffffffffffffffffffffffffffffff)
assume B86
TRANSIENT::MetaKey(name=cvl.label.end, typ=class java.lang.Boolean)=true::
TRANSIENT::MetaKey(name=cvl.label.start, typ=class java.lang.String)=assumptions about extcodesize::
B87 = W37[0xce4604a000000000000000000000002a]>0x0
assume B87
B88 = W37[0xce4604a0000000000000000000000028]>0x0
assume B88
B89 = W37[0xce4604a0000000000000000000000029]>0x0
assume B89
TRANSIENT::MetaKey(name=cvl.label.end, typ=class java.lang.Boolean)=true::
TRANSIENT::MetaKey(name=cvl.label.start, typ=class java.lang.String)=require forall address a. g_readsToAccountContext(a) == 0::
certoraAssume54731 = forall( QVars(a:bv256 bv256) true&&true&&(UR38:uf(a)==0x0))
assume certoraAssume54731
TRANSIENT::MetaKey(name=cvl.label.end, typ=class java.lang.Boolean)=true::
TRANSIENT::MetaKey(name=cvl.label.start, typ=class java.lang.String)=require forall address a1. g_writesToAccountContext(a1) == 0::
certoraAssume54732 = forall( QVars(a1:bv256 bv256) true&&true&&(UR39:uf(a1)==0x0))
assume certoraAssume54732
TRANSIENT::MetaKey(name=cvl.label.end, typ=class java.lang.Boolean)=true::
TRANSIENT::MetaKey(name=cvl.label.start, typ=class java.lang.String)=f(e,args)::
TRANSIENT::MetaKey(name=call.trace.push, typ=class analysis.icfg.Inliner$CallStack$PushRecord)=PushRecord(callee=MethodRef(contractAddress=274184521717934524641157099916833587242, sigHash=SigHash(2eb2c2d6), attr=COMMON), summary=null, id=14)::
M90 = args
tacCalldatabuf!4@14 = R40
tacCalldatabuf!36@14 = R41
tacCalldatabuf!68@14 = R42
tacCalldatabuf!100@14 = R43
tacCalldatabuf!132@14 = R44
B92 = 0xa3s<R45
assume B92
R93 = e.msg.sender
B94 = (0x0<=R93)&&(R93<=0xffffffffffffffffffffffffffffffffffffffff)
assume B94
R95 = e.msg.value
B96 = R46==e.msg.address
assume B96
B97 = (0x0<=R46)&&(R46<=0xffffffffffffffffffffffffffffffffffffffff)
assume B97
B98 = (0x0<=R47)&&(R47<=0xffffffffffffffffffffffffffffffffffffffff)
assume B98
R99 = e.block.timestamp
::Invoke f args :14::
goto: 0_0_0_0_14_0_24786_0

Block 62_0_0_0_0_0_0_0: assume !false
assume !false
TRANSIENT::MetaKey(name=call.trace.pop, typ=class analysis.icfg.Inliner$CallStack$PopRecord)=PopRecord(id=14)::
TRANSIENT::MetaKey(name=cvl.label.end, typ=class java.lang.Boolean)=true::
TRANSIENT::MetaKey(name=cvl.label.start, typ=class java.lang.String)=assert forall address a2. g_readsToAccountContext(a2) == g_writesToAccountContext(a2) && g_readsToAccountContext(a2) <= 1 || g_writesToAccountContext(a2) == 0::
certoraAssert_1 = forall( QVars(a2:bv256 bv256) true&&true&&((true&&true&&true&&true&&(UR7755:uf(a2)==UR9291:uf(a2))&&true&&true&&(UR7755:uf(a2)<=0x1))||(true&&true&&(UR9291:uf(a2)==0x0))))
assert certoraAssert_1,
TRANSIENT::MetaKey(name=cvl.label.end, typ=class java.lang.Boolean)=true::

Block 0_0_0_0_14_0_24786_0: ::14: ERC1155Action.safeBatchTransferFrom::
Previous:
0_0_0_0_0_0_0_0 <-